Library lucas_cubic
Require Export PointsETC.
Open Scope R_scope.
Section Triangle.
Context `{M:triangle_theory}.
Definition sum_cyclic h (x y z:R) := h a b c x y z + h b c a y z x + h c a b z x y.
Definition is_on_lucas_cubic P :=
let h a b c x y z := (b^2+c^2-a^2)*x*(y^2-z^2) in
sum_cyclic h (a×X(P)) (b×Y(P)) (c×Z(P)) = 0.
Lemma X2_is_on_lucas_cubic : is_on_lucas_cubic X_2.
Proof.
intros.
red.
unfold sum_cyclic.
simpl.
ring.
Qed.
End Triangle.
Open Scope R_scope.
Section Triangle.
Context `{M:triangle_theory}.
Definition sum_cyclic h (x y z:R) := h a b c x y z + h b c a y z x + h c a b z x y.
Definition is_on_lucas_cubic P :=
let h a b c x y z := (b^2+c^2-a^2)*x*(y^2-z^2) in
sum_cyclic h (a×X(P)) (b×Y(P)) (c×Z(P)) = 0.
Lemma X2_is_on_lucas_cubic : is_on_lucas_cubic X_2.
Proof.
intros.
red.
unfold sum_cyclic.
simpl.
ring.
Qed.
End Triangle.